CHOICE-STRATEGY-IS: 
UNIT∧EQUALITY[=;3];

EDIT-STRATEGY-IS: 
DEPTH[5]∨LENGTH[4]∨SELDEPTH[F11,3];

ELAPSED-TIME =180100

NIL 1 2
1 ¬A26(F32(THM7,A13),A14)= A14;13 4
2 A26(F32(THM7,A13),A14)= A14;5 6
4 ¬F11(A13,F11(THM7,A25(F32(THM7,A13),A14)))= A14;11 10
5 A(F11(A13,F11(THM7,A25(F32(THM7,A13),A14))));11 12
6 A(F11(A13,F11(THM7,A25(F32(THM7,A13),A14))))⊃A26(F32(THM7,A13),A14)= A14;13 14
10 ¬(F11(A13,W)= A14∧B(W));21 50
11 B(F11(THM7,A25(F32(THM7,A13),A14)));23 24
12 B(W)⊃A(F11(A13,W));25 50
13 F11(A13,F11(THM7,A25(F32(THM7,A13),A14)))= A26(F32(THM7,A13),A14);27 28
14 A(A26(F32(THM7,A13),A14))⊃A26(F32(THM7,A13),A14)= A14;47 30
21 ¬(A14 = X∧(B(W)∧R(A13,W,X)));A1
23 A(A25(F32(THM7,A13),A14));47 40
24 A(W)⊃B(F11(THM7,W));41 50
25 B(X)∧R(A13,X,W)⊃A(W);A1
27 R(F32(THM7,A13),A25(F32(THM7,A13),A14),W)⊃A26(F32(THM7,A13),A14)= W;43 44
28 R(F32(THM7,A13),W,F11(A13,F11(THM7,W)));45 50
30 A(A26(F32(THM7,A13),A14))∧A(A14)⊃A14 = A26(F32(THM7,A13),A14);INSERT
40 A(A14)⊃A(A25(F32(THM7,A13),A14));INSERT
41 A(X)∧R(THM7,X,W)⊃B(W);THM
43 R(F32(THM7,A13),A25(F32(THM7,A13),A14),A26(F32(THM7,A13),A14));47 48
44 R(Y,Z,X)∧R(Y,Z,W)⊃W = X;F2
45 R(THM7,W,X)⊃R(F32(THM7,A13),W,F11(A13,X));49 50
47 A(A14);A1
48 A(A14)⊃R(F32(THM7,A13),A25(F32(THM7,A13),A14),A26(F32(THM7,A13),A14));INSERT
49 R(THM7,W,Y)∧R(A13,Y,X)⊃R(F32(THM7,A13),W,X);INSERT
50 R(W,X,F11(W,X));F1